Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(rev,nil)	→ nil
2:		app(rev,app(app(cons,x),l))	→ app(app(cons,app(app(rev1,x),l)),app(app(rev2,x),l))
3:		app(app(rev1,0),nil)	→ 0
4:		app(app(rev1,app(s,x)),nil)	→ app(s,x)
5:		app(app(rev1,x),app(app(cons,y),l))	→ app(app(rev1,y),l)
6:		app(app(rev2,x),nil)	→ nil
7:		app(app(rev2,x),app(app(cons,y),l))	→ app(rev,app(app(cons,x),app(app(rev2,y),l)))

There are 13 dependency pairs:


8:		APP(rev,app(app(cons,x),l))	→ APP(app(cons,app(app(rev1,x),l)),app(app(rev2,x),l))
9:		APP(rev,app(app(cons,x),l))	→ APP(cons,app(app(rev1,x),l))
10:		APP(rev,app(app(cons,x),l))	→ APP(app(rev1,x),l)
11:		APP(rev,app(app(cons,x),l))	→ APP(rev1,x)
12:		APP(rev,app(app(cons,x),l))	→ APP(app(rev2,x),l)
13:		APP(rev,app(app(cons,x),l))	→ APP(rev2,x)
14:		APP(app(rev1,x),app(app(cons,y),l))	→ APP(app(rev1,y),l)
15:		APP(app(rev1,x),app(app(cons,y),l))	→ APP(rev1,y)
16:		APP(app(rev2,x),app(app(cons,y),l))	→ APP(rev,app(app(cons,x),app(app(rev2,y),l)))
17:		APP(app(rev2,x),app(app(cons,y),l))	→ APP(app(cons,x),app(app(rev2,y),l))
18:		APP(app(rev2,x),app(app(cons,y),l))	→ APP(cons,x)
19:		APP(app(rev2,x),app(app(cons,y),l))	→ APP(app(rev2,y),l)
20:		APP(app(rev2,x),app(app(cons,y),l))	→ APP(rev2,y)

The approximated dependency graph contains one SCC: {8,10,12,14,16,17,19}.

Consider the SCC {8,10,12,14,16,17,19}. By taking the AF π with π(app) = π(APP) = 1 together with the lexicographic path order with precedence rev2 ≻ cons, rev2 ≻ nil, rev2 ≻ rev1 ≻ 0, rev1 ≻ s and rev2 ≈ rev, the rules in {5,7,12,14,16,19} are weakly decreasing and the rules in {1-4,6,8,10,17} are strictly decreasing. There is one new SCC.
- Consider the SCC {12,14,16,19}. The constraints could not be solved.

Tyrolean Termination Tool (0.84 seconds) --- May 4, 2006